<<protocol.m

BMItem[z_] :=
 If[Depth[z]==1, m[z],
  If[z[[0]] === ce, 
   StringJoin[{"mp(", m[z[[1]]], ",", m[z[[2]]], ")"}],
   If[z[[0]] === e,
     m[z[[1]]],
     "???"
   ]
  ]
 ]

BMAnd[x_] :=
 Block[{j},
  If[x === True, "[]",
   If[Depth[x] > 1 && x[[0]] === And,
    strs = Table[BMItem[x[[j]]], {j, 1, Length[x]}];
    Return[StringJoin[{"[", StringJoin[Riffle[strs, ","]], "]"}]],
    StringJoin[{"[", BMItem[x], "]"}]
    ]
   ]
  ]

BMOr[x_] :=
 Block[{j},
  If[x === False, "[]",
   If[Depth[x] > 1 && x[[0]] === Or,
    strs = Table[BMAnd[x[[j]]], {j, 1, Length[x]}];
    Return[StringJoin[{"[", StringJoin[Riffle[strs, ","]], "]"}]],
    StringJoin[{"[", BMAnd[x], "]"}]
    ]
   ]
  ]

DerStr[ix_, c_] :=
 StringJoin[{"dertable(", proto, ",", role, ",", m[ix], ",", BMOr[c], ")."}]


Initial :=
 Array[If[MemberQ[inits, #], True, False] &, ncnd]

celtrans[ix_] :=
 Array[# -> ce[ix, #] && # &, ncnd]

cetrans :=
 Array[
   # -> If[MemberQ[locals, #], False, 
      e[#]] || # || (ces[#] /. celtrans[#]) &
  , ncnd]

appx := Join[{ce[a_, b_] -> ce[a, b], e[a_] -> e[a]}, 
  Array[# -> x[[#]] &, ncnd]]

ApplyRule[rule_] :=
 FullSimplify[
  x[[rule[[1]]]] && ((rule[[2]] /. cpath) /. cetrans) /. appx]

ApplyRules[ix_] := 
 BooleanMinimize[Fold[Or, x[[ix]], Map[ApplyRule, elrules[ix]]], 
  "DNF"]

ApplyTestRules[ix_] := 
 BooleanMinimize[((eltestrules[ix] /. cpath) /. cetrans) /. appx]


x = Initial;

ch = True;
it = 0;
While[ch,
 it++;
 Print["Iteration ", it];
 ch = False;

 For[i = 1, i <= ncnd, i++,
   xn[i] = ApplyRules[i];
   If[xn[i] =!= x[[i]], ch = True]
 ]
 For[i = 1, i <= ncnd, i++, x[[i]] = xn[i]]
]

OutputForm["% derivation table"]>>out

outf=OpenWrite["out"];

For[i = 1, i <= ncnd, i++,
 If[Not[MemberQ[locals, i]],
   ret=ApplyTestRules[i];
   If[ret=!=False, WriteString[outf,DerStr[i,ret],"\n"]]
 ]
]